The work relates to the automatic generation of logical specifications,considered as sets of temporal logic formulas, extracted directly fromdeveloped software models. The extraction process is based on the assumptionthat the whole developed model is structured using only predefined workflowpatterns. A method of automatic transformation of workflow patterns to logicalspecifications is proposed. Applying the presented concepts enables bridgingthe gap between the benefits of deductive reasoning for the correctnessverification process and the difficulties in obtaining complete logicalspecifications for this process.
展开▼
